T:Type, ll:(T List) List.
concat(ll) = nil  T List
 (ll1:(T List) List, l1:T List.
 (concat(ll) = (concat(ll1) @ l1 @ [last(concat(ll))])  T List
 (& ll1 @ [l1 @ [last(concat(ll))]]  ll) 

latex

Definitions

l[i], AB, ij, ||as||, SQType(T), {T}, T, True, p  q, A & B, last(L), P  Q, b, null(as), concat(ll), S  T, Top, x:A. B(x), l1  l2, as @ bs, A, False, Dec(P), P  Q, P  Q, P & Q, x:A. B(x), P  Q, t  T, Prop

Lemmas

assert wf, assert of null, not functionality wrt iff, null wf, decidable assert, concat wf, append wf, not wf, top wf, concat-cons, concat-nil, append nil sq, last wf, iseg wf, last lemma, cons iseg, nil iseg, band wf, and functionality wrt iff, assert of band, iff transitivity, null append, append assoc sq, true wf, squash wf, length wf1, length append, non neg length, length zero, select append back, le wf, select wf